M, A:MsgA, a:Id, p:(A.stateA.da(locl(a))Prop). M.rframe(A.pre p for a)  Prop 

latex

Definitions	M.rframe(A.pre p for a), M.state, M.da(a), (s1  s2 mod x), M.ds(x), 1of(t), 2of(t), MsgA, x:AB(x), State(ds), xdom(f). v=f(x)   P(x;v), x,y. t(x;y), P  Q, left+right, deq-member(eq;x;L), P  Q, A, s = t, P  Q, f(a), {x:A| B(x) }, b, x  dom(f), a:A fp B(a), type List, IdDeq, x:AB(x), f(x)?z, x. t(x), x.A(x), Knd, KindDeq, locl(a), x:A. B(x), Top, Prop, Type, t  T, Id
Lemmas	Id wf, top wf, locl wf, Kind-deq wf, Knd wf, fpf-cap wf, id-deq wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, iff wf, not wf, deq-member wf, fpf-all wf, msga wf